\begin{tabbing}
$\forall$\=${\it poss}$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $T$:Type$_{\mbox{\scriptsize i}}$, $s$:$T$, $i$:Id, $P$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$),\+
\\[0ex]$R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), ${\it Rs}$:($T$$\rightarrow$$T$$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\-\\[0ex](Trans $1$,$2$:$T$. ${\it Rs}$($1$,$2$))
\\[0ex]$\Rightarrow$ (\=$\forall$${\it es}$:ES\{i\}, $e$:E.\+
\\[0ex]${\it poss}$(${\it es}$) $\Rightarrow$ state@$i$ $\subseteq\rho$ $T$ $\Rightarrow$ loc($e$) $=$ $i$ $\Rightarrow$ ${\it Rs}$((state when $e$),state after $e$))
\-\\[0ex]$\Rightarrow$ (\=$\forall$${\it es}$:ES\{i\}.\+
\\[0ex]${\it poss}$(${\it es}$) $\Rightarrow$ state@$i$ $\subseteq\rho$ $T$ $\Rightarrow$ @$i$ stable $s$.ma{-}knows\{i:l\}(${\it poss}$; $i$; $T$; $s$; $P$; ${\it Rs}$; $R$)  )
\-
\end{tabbing}